i, a:Id, T:Type, ds:a:Id fp Type, P:(State(ds)TProp).
@i: (with ds: ds action a:T precondition a(v) is P s v)  Dsys
& (D:Dsys.
& (@i: (with ds: ds action a:T precondition a(v) is P s v)  D
& ( D realizes es. @i Precondition for a(v)P State(ds) (v:T)) 

latex

Definitions

t  T, x:A. B(x), State(ds), x:AB(x), S  T, State(ds), Id, Type, Top, f(x)?z, Prop, S  T, @i Precondition for a(v)P State(ds) (v:T), es is an event system of D, ES, {x:A| B(x) }, x.A(x), {T}, P  Q, x. t(x), Dsys, D1  D2, D realizes es. P(es), A & B, , MsgA, a = b, if b t else f fi, @i: A, a:A fp B(a), @i (with ds: ds action a:T precondition a(v) is P s v), (with ds: ds action a:T precondition a(v) is P s v)

Lemmas

pre-rule, fpf wf, ifthenelse wf, eq id wf, msga wf, ma-single-pre wf, ma-empty wf, Id wf, dsys wf, realizes-monotone-wrt-sub, event system wf, d-es wf, pre-p wf, decl-state wf, ma-state wf